Developing the formal model based on the Event-B design pattern is an excellent method to improve the development efficiency\nof the embedded control system and improve the reusability of the formal model. However, the instantiation of the Event-B design\npattern requires themanual writing of a large number of model codes, which brings a great deal of learning cost and coding burden\nto the engineering staff. In this paper, we propose a modelling approach for formal development of control systems based on the\napplication of iUML-B state machine patterns to model the four synchronization patterns of the typical control system. Then,we use\nthe instantiation of iUML-B pattern state machine to establish a typical multilevel control system's Event-B model.The simulation\nresults show that the event trace of the model obtained using our method is the same as that of the corresponding model obtained\nusing the traditional Event-B design pattern.Compared with the traditional Event-B design pattern method, our method can greatly\nreduce the manual coding burden in the modelling process. The system model expressed using the iUML-B pattern state machine\ncan be easily mapped to the labelled transition system so as to verify the behavioural properties of the model.
Loading....